(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Agent
  imports "HOL-Nominal.Nominal"
begin

lemma pt_id:
  fixes x :: 'a
    and a :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "[(a, a)] ∙ x = x"
proof -
  have "x = ([]::'x prm) ∙ x"
    by(simp add: pt1[OF pt])
  also have "[(a, a)] ∙ x = ([]::'x prm) ∙ x"
    by(simp add: pt3[OF pt] at_ds1[OF at])
  finally show ?thesis by simp
qed

lemma pt_swap:
  fixes x :: 'a
  and a :: 'x
  and b :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"

  shows "[(a, b)] ∙ x = [(b, a)] ∙ x"
proof -
  show ?thesis by(simp add: pt3[OF pt] at_ds5[OF at])
qed

atom_decl name

lemmas name_fresh_abs = fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fs_name1]
lemmas name_bij = at_bij[OF at_name_inst]
lemmas name_supp_abs = abs_fun_supp[OF pt_name_inst, OF at_name_inst, OF fs_name1]
lemmas name_abs_eq = abs_fun_eq[OF pt_name_inst, OF at_name_inst]
lemmas name_supp = at_supp[OF at_name_inst]
lemmas name_calc = at_calc[OF at_name_inst]
lemmas name_fresh_fresh = pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]
lemmas name_fresh_left = pt_fresh_left[OF pt_name_inst, OF at_name_inst]
lemmas name_fresh_right = pt_fresh_right[OF pt_name_inst, OF at_name_inst]
lemmas name_id[simp] = pt_id[OF pt_name_inst, OF at_name_inst]
lemmas name_swap_bij[simp] = pt_swap_bij[OF pt_name_inst, OF at_name_inst]
lemmas name_swap = pt_swap[OF pt_name_inst, OF at_name_inst]
lemmas name_rev_per = pt_rev_pi[OF pt_name_inst, OF at_name_inst]
lemmas name_per_rev = pt_pi_rev[OF pt_name_inst, OF at_name_inst]
lemmas name_exists_fresh = at_exists_fresh[OF at_name_inst, OF fs_name1]
lemmas name_perm_compose = pt_perm_compose[OF pt_name_inst, OF at_name_inst]

nominal_datatype pi = PiNil                  ("𝟬")
                    | Output name name pi    ("_{_}._" [120, 120, 110] 110)
                    | Tau pi                 ("τ._" [120] 110)
                    | Input name "«name» pi" ("_<_>._" [120, 120, 110] 110)
                    | Match name name pi     ("[_⌢_]_" [120, 120, 110] 110)
                    | Mismatch name name pi  ("[_≠_]_" [120, 120, 110] 110)
                    | Sum pi pi              (infixr "⊕" 90)
                    | Par pi pi              (infixr "∥" 85)
                    | Res "«name» pi"        ("<ν_>_" [100, 100] 100)
                    | Bang pi                ("!_" [110] 110)

lemmas name_fresh[simp] = at_fresh[OF at_name_inst]

lemma alphaInput:
  fixes a :: name
  and   x :: name
  and   P :: pi
  and   c :: name

  assumes A1: "c ♯ P"

  shows "a<x>.P = a<c>.([(x, c)] ∙ P)"
proof(cases "x = c")
  assume "x=c"
  thus ?thesis by(simp)
next
  assume "x ≠ c"
  with A1 show ?thesis
    by(simp add: pi.inject alpha name_fresh_left name_calc)
qed

lemma alphaRes:
  fixes a :: name
  and   P :: pi
  and   c :: name
  
  assumes A1: "c ♯ P"

  shows "<νa>P = <νc>([(a, c)] ∙ P)"
proof(cases "a=c")
  assume "a=c"
  thus ?thesis by simp
next
  assume "a ≠ c"
  with A1 show ?thesis
    by(simp add: pi.inject alpha fresh_left name_calc)
qed

(*Substitution*)

definition subst_name :: "name ⇒ name ⇒ name ⇒ name"   ("_[_::=_]" [110, 110, 110] 110)
where
  "a[b::=c] ≡ if (a = b) then c else a"

declare subst_name_def[simp]

lemma subst_name_eqvt[eqvt]:
  fixes p :: "name prm"
  and   a :: name
  and   b :: name
  and   c :: name

  shows "p ∙ (a[b::=c]) = (p∙ a)[(p ∙ b)::=(p ∙ c)]"
by(auto simp add: at_bij[OF at_name_inst])


nominal_primrec (freshness_context: "(c::name, d::name)")
  subs :: "pi ⇒ name ⇒ name ⇒ pi" ("_[_::=_]" [100,100,100] 100)
where
  "𝟬[c::=d] = 𝟬"
| "τ.(P)[c::=d] = τ.(P[c::=d])"
| "a{b}.P[c::=d] = (a[c::=d]){(b[c::=d])}.(P[c::=d])"
| "⟦x ≠ a; x ≠ c; x ≠ d⟧ ⟹ (a<x>.P)[c::=d] = (a[c::=d])<x>.(P[c::=d])"
| "[a⌢b]P[c::=d] = [(a[c::=d])⌢(b[c::=d])](P[c::=d])"
| "[a≠b]P[c::=d] = [(a[c::=d])≠(b[c::=d])](P[c::=d])"
| "(P ⊕ Q)[c::=d] = (P[c::=d]) ⊕ (Q[c::=d])"
| "(P ∥ Q)[c::=d] = (P[c::=d]) ∥ (Q[c::=d])"
| "⟦x ≠ c; x ≠ d⟧ ⟹ (<νx>P)[c::=d] = <νx>(P[c::=d])"
| "!P[c::=d] = !(P[c::=d])"
apply(simp_all add: abs_fresh)
apply(finite_guess)+
by(fresh_guess)+

lemma forget:
  fixes a :: name
  and   P :: pi
  and   b :: name

  assumes "a ♯ P"

  shows "P[a::=b] = P"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)

lemma fresh_fact2[rule_format]:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "a ≠ b"

  shows "a ♯ P[a::=b]"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)

lemma subst_identity[simp]:
  fixes P :: pi
  and   a :: name

  shows "P[a::=a] = P"
by(nominal_induct P avoiding: a rule: pi.strong_induct) auto

lemma renaming:
  fixes P :: pi
  and   a :: name
  and   b :: name
  and   c :: name

  assumes "c ♯ P"

  shows "P[a::=b] = ([(c, a)] ∙ P)[c::=b]"
using assms
by(nominal_induct P avoiding: a b c rule: pi.strong_induct)
  (auto simp add: name_calc name_fresh_abs)


lemma fresh_fact1:
  fixes P :: pi
  and   a :: name
  and   b :: name
  and   c :: name

  assumes "a ♯ P"
  and     "a ≠ c"

  shows "a ♯ P[b::=c]"
using assms
by(nominal_induct P avoiding: a b c rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)


lemma eqvt_subs[eqvt]:
  fixes p :: "name prm"
  and   P :: pi
  and   a :: name
  and   b :: name

  shows "p ∙ (P[a::=b]) = (p ∙ P)[(p ∙ a)::=(p ∙ b)]"
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_bij)


lemma substInput[simp]:
  fixes x :: name
  and   b :: name
  and   c :: name
  and   a :: name
  and   P :: pi

  assumes "x ≠ b"
  and     "x ≠ c"

  shows "(a<x>.P)[b::=c] = (a[b::=c])<x>.(P[b::=c])"
proof -
  obtain y::name where"y ≠ a" and "y ♯ P" and "y ≠ b" and "y ≠ c"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹y ♯ P› have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  moreover have "(a[b::=c])<x>.(P[b::=c]) = (a[b::=c])<y>.(([(x, y)] ∙ P)[b::=c])" (is "?LHS = ?RHS")
  proof -
    from ‹y ♯ P› ‹y ≠ c› have "y ♯ P[b::=c]" by(rule fresh_fact1)
    hence "?LHS = (a[b::=c])<y>.([(x, y)] ∙ (P[b::=c]))" by(simp add: alphaInput)
    moreover with ‹x ≠ b› ‹x ≠ c› ‹y ≠ b› ‹y ≠ c› have "… = ?RHS"
      by(auto simp add: eqvt_subs name_calc)
    ultimately show ?thesis by simp
  qed
  ultimately show ?thesis using ‹y ≠ a› ‹y ≠ b› ‹y ≠ c› by simp
qed

lemma injPermSubst:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "[(a, b)] ∙ P = P[a::=b]"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_calc name_fresh_abs)

lemma substRes2:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "<νa>P = <νb>(P[a::=b])"
proof(case_tac "a = b")
  assume "a = b"
  thus ?thesis by auto
next
  assume "a ≠ b"
  moreover with ‹b ♯ P› show ?thesis
    apply(simp add: pi.inject abs_fun_eq[OF pt_name_inst, OF at_name_inst])
    apply auto
    apply(simp add: renaming)
    apply(simp add: pt_swap[OF pt_name_inst, OF at_name_inst])
    apply(simp add: renaming)
    apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
    by(force simp add: at_calc[OF at_name_inst])
qed

lemma freshRes:
  fixes P :: pi
  and   a :: name
  
  shows "a ♯ <νa>P"
by(simp add: name_fresh_abs)

lemma substRes3: 
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "(<νa>P)[a::=b] = <νb>(P[a::=b])"
proof -
  have "(<νa>P)[a::=b] = <νa>P"
    using freshRes by(simp add: forget)
  thus ?thesis using ‹b ♯ P› by(simp add: substRes2)
qed

lemma suppSubst:
  fixes P :: pi
  and   a :: name
  and   b :: name

  shows "supp(P[a::=b]) ⊆ insert b ((supp P) - {a})"
apply(nominal_induct P avoiding: a b rule: pi.strong_induct,
      simp_all add: pi.supp name_supp_abs name_supp supp_prod)
by(blast)+
  
(******** Sequential substitution *******)

primrec seqSubs :: "pi ⇒ (name × name) list ⇒ pi" ("_[<_>]" [100,100] 100) where
  "P[<[]>] = P"
| "P[<(x#σ)>] = (P[(fst x)::=(snd x)])[<σ>]"

primrec seq_subst_name :: "name ⇒ (name × name) list ⇒ name" where
  "seq_subst_name a [] = a"
| "seq_subst_name a (x#σ) = seq_subst_name (a[(fst x)::=(snd x)]) σ"

lemma freshSeqSubstName:
  fixes x :: name
  and   a :: name
  and   s :: "(name × name) list"

  assumes "x ≠ a"
  and     "x ♯ s"

  shows "x ≠ seq_subst_name a s"
using assms
apply(induct s arbitrary: a)
apply simp
apply(case_tac "aa = fst(a)")
by (force simp add: fresh_list_cons fresh_prod)+


lemma seqSubstZero[simp]:
  fixes σ :: "(name × name) list"

  shows "𝟬[<σ>] = 𝟬"
by(induct σ, auto)

lemma seqSubstTau[simp]:
  fixes P :: pi
  and   σ :: "(name × name) list"

  shows "(τ.(P))[<σ>] = τ.(P[<σ>])"
by(induct σ arbitrary: P, auto)

lemma seqSubstOutput[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"
  
  shows "(a{b}.P)[<σ>] = (seq_subst_name a σ){(seq_subst_name b σ)}.(P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  assumes "x ♯ σ"
 
  shows "(a<x>.P)[<σ>] = (seq_subst_name a σ)<x>.(P[<σ>])"
using assms
by(induct σ arbitrary: a x P) (auto simp add: fresh_list_cons fresh_prod)

lemma seqSubstMatch[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  shows "([a⌢b]P)[<σ>] = [(seq_subst_name a σ)⌢(seq_subst_name b σ)](P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstMismatch[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  shows "([a≠b]P)[<σ>] = [(seq_subst_name a σ)≠(seq_subst_name b σ)](P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstSum[simp]:
  fixes P :: pi
  and   Q :: pi
  and   σ :: "(name × name) list"

  shows "(P ⊕ Q)[<σ>] = (P[<σ>]) ⊕ (Q[<σ>])"
by(induct σ arbitrary: P Q , auto)

lemma seqSubstPar[simp]:
  fixes P :: pi
  and   Q :: pi
  and   σ :: "(name × name) list"

  shows "(P ∥ Q)[<σ>] = (P[<σ>]) ∥ (Q[<σ>])"
by(induct σ arbitrary: P Q, auto)

lemma seqSubstRes[simp]:
  fixes x :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  assumes "x ♯ σ"

  shows "(<νx>P)[<σ>] = <νx>(P[<σ>])"
using assms
by(induct σ arbitrary: x P) (auto simp add: fresh_list_cons fresh_prod)

lemma seqSubstBang[simp]:
  fixes P :: pi
  and   s :: "(name × name) list"

  shows "(!P)[<σ>] = !(P[<σ>])"
by(induct σ arbitrary: P, auto)

lemma seqSubstEqvt[eqvt, simp]:
  fixes P :: pi
  and   σ :: "(name × name) list"
  and   p :: "name prm"

  shows "p ∙ (P[<σ>]) = (p ∙ P)[<(p ∙ σ)>]"
by(induct σ arbitrary: P, auto simp add: eqvt_subs)

lemma seqSubstAppend[simp]:
  fixes P  :: pi
  and   σ  :: "(name × name) list"
  and   σ' :: "(name × name) list"

  shows "P[<(σ@σ')>] = (P[<σ>])[<σ'>]"
by(induct σ arbitrary: P, auto)

lemma freshSubstChain[intro]:
  fixes P :: pi
  and   σ :: "(name × name) list"
  and   a :: name

  assumes "a ♯ P"
  and     "a ♯ σ"

  shows "a ♯ P[<σ>]"
using assms
by(induct σ arbitrary: a P, auto simp add: fresh_list_cons fresh_prod fresh_fact1)

end

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Late_Semantics
  imports Agent
begin
 
nominal_datatype subject = InputS name
                         | BoundOutputS name

nominal_datatype freeRes = OutputR name name             ("_[_]" [130, 130] 110)
                         | TauR                          ("τ" 130)

nominal_datatype residual = BoundR subject "«name» pi" ("_«_» ≺ _" [80, 80, 80] 80)
                          | FreeR freeRes pi           ("_ ≺ _" [80, 80] 80)

lemmas residualInject = residual.inject freeRes.inject subject.inject

abbreviation "Transitions_Inputjudge" :: "name ⇒ name ⇒ pi ⇒ residual" ("_<_> ≺ _" [80, 80, 80] 80)
where "a<x> ≺ P' ≡ ((InputS a)«x» ≺ P')"

abbreviation "Transitions_BoundOutputjudge" :: "name ⇒ name ⇒ pi ⇒ residual" ("_<ν_> ≺ _" [80, 80, 80] 80)
where "a<νx> ≺ P' ≡ (BoundR (BoundOutputS a) x P')"

inductive transitions :: "pi ⇒ residual ⇒ bool"      ("_ ⟼ _" [80, 80] 80)
where
  Tau:               "τ.(P) ⟼ τ ≺ P"
| Input:             "x ≠ a ⟹ a<x>.P ⟼ a<x> ≺ P"
| Output:            "a{b}.P ⟼ a[b] ≺  P"
 
| Match:             "⟦P ⟼ Rs⟧ ⟹ [b⌢b]P ⟼ Rs"
| Mismatch:          "⟦P ⟼ Rs; a ≠ b⟧ ⟹ [a≠b]P ⟼ Rs"

| Open:              "⟦P ⟼ a[b] ≺ P'; a ≠ b⟧ ⟹ <νb>P ⟼ a<νb> ≺ P'"
| Sum1:              "⟦P ⟼ Rs⟧ ⟹ (P ⊕ Q) ⟼ Rs"
| Sum2:              "⟦Q ⟼ Rs⟧ ⟹ (P ⊕ Q) ⟼ Rs"

| Par1B:             "⟦P ⟼ a«x» ≺ P'; x ♯ P; x ♯ Q; x ♯ a⟧ ⟹ P ∥ Q ⟼ a«x» ≺ (P' ∥ Q)"
| Par1F:             "⟦P ⟼ α ≺ P'⟧ ⟹ P ∥ Q ⟼ α ≺ (P' ∥ Q)"
| Par2B:             "⟦Q ⟼ a«x» ≺ Q'; x ♯ P; x ♯ Q; x ♯ a⟧ ⟹ P ∥ Q ⟼ a«x» ≺ (P ∥ Q')"
| Par2F:             "⟦Q ⟼ α ≺ Q'⟧ ⟹ P ∥ Q ⟼ α ≺ (P ∥ Q')"

| Comm1:             "⟦P ⟼ a<x> ≺ P'; Q ⟼ a[b] ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ≠ b; x ♯ Q'⟧ ⟹ P ∥ Q ⟼ τ ≺ P'[x::=b] ∥ Q'"
| Comm2:             "⟦P ⟼ a[b] ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ≠ b; x ♯ P'⟧ ⟹ P ∥ Q ⟼ τ ≺ P' ∥ Q'[x::=b]"
| Close1:            "⟦P ⟼ a<x> ≺ P'; Q ⟼ a<νy> ≺ Q'; x ♯ P; x ♯ Q; y ♯ P; 
                       y ♯ Q; x ≠ a; x ♯ Q'; y ≠ a; y ♯ P'; x ≠ y⟧ ⟹ P ∥ Q ⟼ τ ≺ <νy>(P'[x::=y] ∥ Q')"
| Close2:            "⟦P ⟼ a<νy> ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ P; x ♯ Q; y ♯ P;
                       y ♯ Q; x ≠ a; x ♯ P'; y ≠ a; y ♯ Q'; x ≠ y⟧ ⟹ P ∥ Q ⟼ τ ≺ <νy>(P' ∥ Q'[x::=y])"

| ResB:              "⟦P ⟼ a«x» ≺ P'; y ♯ a; y ≠ x; x ♯ P; x ♯ a⟧ ⟹ <νy>P ⟼ a«x» ≺ <νy>P'"
| ResF:              "⟦P ⟼ α ≺ P'; y ♯ α⟧ ⟹ <νy>P ⟼ α ≺ <νy>P'"

| Bang:              "⟦P ∥ !P ⟼ Rs⟧ ⟹ !P ⟼ Rs"

equivariance transitions
nominal_inductive transitions
by(auto simp add: abs_fresh fresh_fact2)

lemma alphaBoundResidual:
  fixes a  :: subject
  and   x  :: name
  and   P  :: pi
  and   x' :: name

  assumes A1: "x' ♯ P"

  shows "a«x» ≺ P = a«x'» ≺ ([(x, x')] ∙ P)"
proof(cases "x=x'")
  assume "x=x'"
  thus ?thesis by simp
next
  assume "x ≠ x'"
  with A1 show ?thesis
    by(simp add: residualInject alpha name_fresh_left name_calc)
qed

lemma freshResidual:
  fixes P  :: pi
  and   Rs :: residual
  and   x  :: name
  
  assumes "P ⟼ Rs"
  and     "x ♯ P"

  shows "x ♯ Rs"
using assms
by(nominal_induct rule: transitions.strong_induct)
  (auto simp add: abs_fresh fresh_fact2 fresh_fact1)

lemma freshBoundDerivative:
  assumes "P ⟼a«x» ≺ P'"
  and     "y ♯ P"

  shows "y ♯ a"
  and   "y ≠ x ⟹ y ♯ P'"
apply -
using assms
by(fastforce dest: freshResidual simp add: abs_fresh)+

lemma freshFreeDerivative:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   y  :: name

  assumes "P ⟼α ≺ P'"
  and     "y ♯ P"

  shows "y ♯ α"
  and   "y ♯ P'"
apply -
using assms
by(fastforce dest: freshResidual)+

lemma substTrans[simp]: 
  fixes b :: name
  and   P :: pi
  and   a :: name
  and   c :: name

  assumes "b ♯ P"

  shows "(P[a::=b])[b::=c] = P[a::=c]"
using assms
apply(simp add: injPermSubst[THEN sym])
apply(simp add: renaming)
by(simp add: pt_swap[OF pt_name_inst, OF at_name_inst])

lemma Input:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "a<x>.P ⟼a<x> ≺ P"
proof -
  obtain y::name where "y ≠ a" and "y ♯ P"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from ‹y ♯ P› have "a<x>.P = a<y>.([(x, y)] ∙ P)" and "a<x> ≺ P = a<y> ≺ ([(x, y)] ∙ P)"
    by(auto simp add: alphaBoundResidual alphaInput)
  with ‹y ≠ a› show ?thesis by(force intro: Input)
qed

declare perm_fresh_fresh[simp] name_swap[simp] fresh_prod[simp]

lemma Par1B:
  fixes P  :: pi
  and   a  :: subject
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi

  assumes "P ⟼a«x» ≺ P'"
  and     "x ♯ Q"

  shows "P ∥ Q ⟼a«x» ≺ P' ∥ Q"
proof -
  obtain y::name where "y ♯ P" and "y ♯ P'" and "y ♯ Q" and "y ♯ a"
    by(generate_fresh "name", auto)
  from ‹P ⟼ a«x» ≺ P'› ‹y ♯ P'› have "P ⟼a«y» ≺ ([(x, y)] ∙ P')"
    by(simp add: alphaBoundResidual)
  hence "P ∥ Q ⟼a«y» ≺ ([(x, y)] ∙ P') ∥ Q" using ‹y ♯ P› ‹y ♯ Q› ‹y ♯ a›
    by(rule Par1B)
  with ‹x ♯ Q› ‹y ♯ P'› ‹y ♯ Q› show ?thesis
    by(subst alphaBoundResidual[where x'=y]) auto
qed

lemma Par2B:
  fixes Q  :: pi
  and   a  :: subject
  and   x  :: name
  and   Q' :: pi
  and   P  :: pi

  assumes QTrans: "Q ⟼a«x» ≺ Q'"
  and     "x ♯ P"

  shows "P ∥ Q ⟼a«x» ≺ P ∥ Q'"
proof -
  obtain y::name where "y ♯ Q" and "y ♯ Q'" and "y ♯ P" and "y ♯ a"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from QTrans ‹y ♯ Q'› have "Q ⟼a«y» ≺ ([(x, y)] ∙ Q')"
    by(simp add:alphaBoundResidual)
  hence "P ∥ Q ⟼a«y» ≺ P ∥ ([(x, y)] ∙ Q')" using ‹y ♯ P› ‹y ♯ Q› ‹y ♯ a›
    by(rule Par2B)
  moreover have "a«y» ≺ P ∥ ([(x, y)] ∙ Q') = a«x» ≺ P ∥ Q'"
  proof -
    from ‹y ♯ Q'› ‹x ♯ P› have "x ♯ P ∥ ([(x, y)] ∙ Q')" by(auto simp add: calc_atm fresh_left)
    with ‹x ♯ P› ‹y ♯ P› show ?thesis by(simp only: alphaBoundResidual, auto simp add: name_swap name_fresh_fresh)
  qed
  ultimately show ?thesis by simp
qed

lemma Comm1:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   b  :: name
  and   Q' :: pi

  assumes PTrans: "P ⟼a<x> ≺ P'"
  and     QTrans: "Q ⟼a[b] ≺ Q'"

  shows "P ∥ Q ⟼τ ≺ P'[x::=b] ∥ Q'"
proof -
  obtain y::name where "y ♯ P" and "y ♯ P'" and "y ♯ Q" and "y ≠ a" and "y ≠ b" and "y ♯ Q'"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from PTrans ‹y ♯ P'› have "P ⟼a<y> ≺ ([(x, y)] ∙ P')"
    by(simp add: alphaBoundResidual)
  hence "P ∥ Q ⟼τ ≺ ([(x, y)] ∙ P')[y::=b] ∥ Q'" 
    using QTrans ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a› ‹y ≠ b› ‹y ♯ Q'› 
    by(rule Comm1)
  with ‹y ♯ P'› show ?thesis by(simp add: renaming name_swap)
qed

lemma Comm2:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   Q  :: pi
  and   x  :: name
  and   Q' :: pi

  assumes PTrans: "P ⟼a[b] ≺ P'"
  and     QTrans: "Q ⟼a<x> ≺ Q'"

  shows "P ∥ Q ⟼τ ≺ P' ∥ (Q'[x::=b])"
proof -
  obtain y::name where "y ♯ P" and "y ♯ P'" and "y ♯ Q" and "y ≠ a" and "y ≠ b" and "y ♯ Q'"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from QTrans ‹y ♯ Q'› have "Q ⟼a<y> ≺ ([(x, y)] ∙ Q')"
    by(simp add: alphaBoundResidual)
  with PTrans have "P ∥ Q ⟼τ ≺ P' ∥ (([(x, y)] ∙ Q')[y::=b])"
  using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a› ‹y ≠ b› ‹y ♯ P'›
    by(rule Comm2)
  with ‹y ♯ Q'› show ?thesis by(simp add: renaming name_swap)
qed

lemma Close1:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   y  :: name
  and   Q' :: pi

  assumes PTrans: "P ⟼a<x> ≺ P'"
  and     QTrans: "Q ⟼a<νy> ≺ Q'"
  and     "y ♯ P"

  shows "P ∥ Q ⟼τ ≺ <νy>(P'[x::=y] ∥ Q')"
proof - 
  obtain x'::name where "x' ♯ P" and "x' ♯ P'" and "x' ♯ Q" and "x' ♯ Q'" and "x' ≠ a"
    by(generate_fresh "name", auto simp add: fresh_prod)
  obtain y'::name where "y' ♯ P" and "y' ♯ Q'" and "y' ♯ Q"
                    and "y' ♯ P'" and "y' ≠ x'" and "y' ≠ y" and "y' ≠ a"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from PTrans ‹x' ♯ P'› have "P ⟼a<x'> ≺ ([(x, x')] ∙ P')"
    by(simp add: alphaBoundResidual)
  moreover from QTrans ‹y' ♯ Q'› have "Q ⟼a<νy'> ≺ ([(y, y')] ∙ Q')"
    by(simp add: alphaBoundResidual)
  ultimately have "P ∥ Q ⟼τ ≺ <νy'>(([(x, x')] ∙ P')[x'::=y'] ∥ ([(y, y')] ∙ Q'))"
    using ‹y' ♯ P› ‹y' ♯ Q› ‹x' ♯ P› ‹x' ♯ Q› ‹y' ≠ x'› ‹y' ≠ a› ‹x' ≠ a›
          ‹y' ♯ P'› ‹y' ♯ Q'› ‹x' ♯ P'› ‹x' ♯ Q'›
    apply(rule_tac Close1)
    by assumption (auto simp add: fresh_left calc_atm)
  moreover have "<νy'>(([(x, x')] ∙ P')[x'::=y'] ∥ ([(y, y')] ∙ Q')) = <νy>(P'[x::=y] ∥ Q')"
  proof -
    from ‹x' ♯ P'› have "([(x, x')] ∙ P')[x'::=y'] = P'[x::=y']" by(simp add: renaming name_swap)
    moreover have "y ♯ (P'[x::=y'] ∥ ([(y, y')] ∙ Q'))"
    proof(case_tac "y = x")
      assume "y = x"
      with ‹y' ♯ Q'› ‹y' ≠ y› show ?thesis by(auto simp add: fresh_fact2 fresh_left calc_atm)
    next
      assume "y ≠ x"
      with ‹y ♯ P› PTrans have "y ♯ P'" by(force dest: freshBoundDerivative)
      with ‹y' ♯ Q'› ‹y' ≠ y› show ?thesis by(auto simp add: fresh_left calc_atm fresh_fact1)
    qed
    ultimately show ?thesis using ‹y' ♯ P'› apply(simp only: alphaRes)
      by(auto simp add: name_swap eqvt_subs calc_atm renaming)
  qed
  ultimately show ?thesis by simp
qed

lemma Close2:
  fixes P  :: pi
  and   a  :: name
  and   y  :: name
  and   P' :: pi
  and   Q  :: pi
  and   x  :: name
  and   Q' :: pi

  assumes PTrans: "P ⟼a<νy> ≺ P'"
  and     QTrans: "Q ⟼a<x> ≺ Q'"
  and     "y ♯ Q"

  shows "P ∥ Q ⟼τ ≺ <νy>(P' ∥ (Q'[x::=y]))"
proof -
  obtain x'::name where "x' ♯ P" and "x' ♯ Q'" and "x' ♯ Q" and "x' ♯ P'" and "x' ≠ a"
    by(generate_fresh "name", auto simp add: fresh_prod)
  obtain y'::name where "y' ♯ P" and "y' ♯ P'" and "y' ♯ Q"
                    and "y' ♯ Q'" and "y' ≠ x'" and "y' ≠ y" and "y' ≠ a"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from PTrans ‹y' ♯ P'› have "P ⟼a<νy'> ≺ ([(y, y')] ∙ P')"
    by(simp add: alphaBoundResidual)
  moreover from QTrans ‹x' ♯ Q'› have "Q ⟼a<x'> ≺ ([(x, x')] ∙ Q')"
    by(simp add: alphaBoundResidual)
  ultimately have "P ∥ Q ⟼τ ≺ <νy'>(([(y, y')] ∙ P') ∥ (([(x, x')] ∙ Q')[x'::=y']))"
    using ‹y' ♯ P› ‹y' ♯ Q› ‹x' ♯ P› ‹x' ♯ Q› ‹y' ≠ x'› ‹x' ≠ a› ‹y' ≠ a›
          ‹x' ♯ P'› ‹x' ♯ Q'› ‹y' ♯ P'› ‹y' ♯ Q'›
    by(rule_tac Close2) (assumption | auto simp add: fresh_left calc_atm)+
  moreover have "<νy'>(([(y, y')] ∙ P') ∥ (([(x, x')] ∙ Q')[x'::=y'])) = <νy>(P' ∥ (Q'[x::=y]))"
  proof -
    from ‹x' ♯ Q'› have "([(x, x')] ∙ Q')[x'::=y'] = Q'[x::=y']" by(simp add: renaming name_swap)
    moreover have "y ♯ (([(y, y')] ∙ P') ∥ (Q'[x::=y']))"
    proof(case_tac "y = x")
      assume "y = x"
      with ‹y' ♯ P'› ‹y' ≠ y› show ?thesis by(auto simp add: fresh_fact2 fresh_left calc_atm)
    next
      assume "y ≠ x"
      with ‹y ♯ Q› QTrans have "y ♯ Q'" by(force dest: freshBoundDerivative)
      with ‹y' ♯ P'› ‹y' ≠ y› show ?thesis by(auto simp add: fresh_left calc_atm fresh_fact1)
    qed
    ultimately show ?thesis using ‹y' ♯ Q'› apply(simp only: alphaRes)
      by(auto simp add: name_swap eqvt_subs calc_atm renaming)
  qed
  ultimately show ?thesis by simp
qed

lemma ResB: 
  fixes P  :: pi
  and   a  :: subject
  and   x  :: name
  and   P' :: pi
  and   y  :: name

  assumes PTrans: "P ⟼a«x» ≺ P'"
  and     "y ♯ a"
  and     "y ≠ x"

  shows "<νy>P ⟼a«x» ≺ <νy>P'"
proof -
  obtain z where "z ♯ P" and "z ♯ a" and "z ≠ y" and "z ♯ P'"
    by(generate_fresh "name", auto simp add: fresh_prod)
  from PTrans ‹z ♯ P'›  have "P ⟼a«z» ≺ ([(x, z)] ∙ P')" by(simp add: alphaBoundResidual)
  with ‹z ♯ P› ‹z ♯ a› ‹z ≠ y› ‹y ♯ a› have "<νy>P ⟼a«z» ≺ <νy>([(x, z)] ∙ P')" by(rule_tac ResB) auto
  moreover have "a«z» ≺ <νy>([(x, z)] ∙ P') = a«x» ≺ <νy>P'"
  proof -
    from ‹z ♯ P'› ‹y ≠ x› have "x ♯ <νy>([(x, z)] ∙ P')" by(auto simp add: abs_fresh fresh_left calc_atm)
    with ‹y ≠ x› ‹z ≠ y› show ?thesis by(simp add: alphaBoundResidual name_swap calc_atm)
  qed
  ultimately show ?thesis by simp
qed

lemma outputInduct[consumes 1, case_names Output Match Mismatch Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   F  :: "'a::fs_name ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P ⟼a[b] ≺ P'"
  and     "⋀a b P C. F C (a{b}.P) a b P"
  and     "⋀P a b P' c C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C ([c⌢c]P) a b P'"
  and     "⋀P a b P' c d C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'; c ≠ d⟧ ⟹ F C ([c≠d]P) a b P'"
  and     "⋀P a b P' Q C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C (P ⊕ Q) a b P'"
  and     "⋀Q a b Q' P C. ⟦Q ⟼OutputR a b ≺ Q'; ⋀C. F C Q a b Q'⟧ ⟹ F C (P ⊕ Q) a b Q'"
  and     "⋀P a b P' Q C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C (P ∥ Q) a b (P' ∥ Q)"
  and     "⋀Q a b Q' P C. ⟦Q ⟼OutputR a b ≺ Q'; ⋀C. F C Q a b Q'⟧ ⟹ F C (P ∥ Q) a b (P ∥ Q')"
  and     "⋀P a b P' x C. ⟦P ⟼OutputR a b ≺ P'; x ≠ a; x ≠ b; x ♯ C; ⋀C. F C P a b P'⟧ ⟹
                            F C (<νx>P) a b (<νx>P')"
  and     "⋀P a b P' C. ⟦P ∥ !P ⟼OutputR a b ≺ P'; ⋀C. F C (P ∥ !P) a b P'⟧ ⟹ F C (!P) a b P'"

  shows "F C P a b P'"
proof -
  from Trans show ?thesis
  by(nominal_induct x2 == "OutputR a b ≺ P'" avoiding: C arbitrary: P' rule: transitions.strong_induct,
     auto simp add: residualInject freeRes.inject intro: assms)
qed

lemma inputInduct[consumes 2, case_names Input Match Mismatch Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   F  :: "('a::fs_name) ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes a: "P ⟼a<x> ≺ P'"
  and       "x ♯ P"
  and     cInput:    "⋀a x P C. F C (a<x>.P) a x P"
  and     cMatch:    "⋀P a x P' b C. ⟦P ⟼a<x> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C ([b⌢b]P) a x P'"
  and     cMismatch: "⋀P a x P' b  c C. ⟦P ⟼a<x> ≺ P'; ⋀C. F C P a x P'; b ≠ c⟧ ⟹ F C ([b≠c]P) a x P'"
  and     cSum1:     "⋀P Q a x P' C. ⟦P ⟼a<x> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C (P ⊕ Q) a x P'" 
  and     cSum2:     "⋀P Q a x Q' C. ⟦Q ⟼a<x> ≺ Q'; ⋀C. F C Q a x Q'⟧ ⟹ F C (P ⊕ Q) a x Q'" 
  and     cPar1B:    "⋀P P' Q a x C. ⟦P ⟼a<x> ≺ P'; x ♯ P; x ♯ Q; x ≠ a; ⋀C. F C P a x P'⟧ ⟹
                                       F C (P ∥ Q) a x (P' ∥ Q)" 
  and     cPar2B:    "⋀P Q Q' a x C. ⟦Q ⟼a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; ⋀C. F C Q a x Q'⟧ ⟹
                                       F C (P ∥ Q) a x (P ∥ Q')"
  and     cResB:     "⋀P P' a x y C. ⟦P ⟼a<x> ≺ P'; y ≠ a; y ≠ x; y ♯ C;
                                      ⋀C. F C P a x P'⟧ ⟹ F C (<νy>P) a x (<νy>P')"
  and     cBang:     "⋀P a x P' C. ⟦P ∥ !P ⟼a<x> ≺ P'; ⋀C. F C (P ∥ !P) a x P'⟧ ⟹
                                     F C (!P) a x P'"
  shows "F C P a x P'"
proof -
  from a ‹x ♯ P› show ?thesis
  proof(nominal_induct x2 == "a<x> ≺ P'" avoiding: C a x P' rule: transitions.strong_induct)
    case(Tau P)
    thus ?case by(simp add: residualInject)
  next
    case(Input x a P C a' x' P')
    have "x ♯ x'" by fact hence "x ≠ x'" by simp
    moreover have "a<x> ≺ P = a'<x'> ≺ P'" by fact
    ultimately have aeqa': "a = a'" and PeqP': "P = [(x, x')] ∙ P'"
      by(simp add: residualInject freeRes.inject subject.inject name_abs_eq)+
    
    have "F C (a<x'>.([(x, x')] ∙ P)) a x' ([(x, x')] ∙ P)" by(rule cInput)
    moreover have "x ♯ P'" by fact
    ultimately show ?case using PeqP' aeqa' by(simp add: alphaInput name_swap)
  next
    case(Output P a b)
    thus ?case by(simp add: residualInject)
  next
    case(Match P b Rs a x)
    thus ?case 
      by(force intro: cMatch simp add: residualInject) 
  next
    case(Mismatch P Rs a b C a x)
    thus ?case 
      by(force intro: cMismatch simp add: residualInject) 
  next
    case(Open P P' a b C a' x P')
    thus ?case by(simp add: residualInject)
  next
    case(Sum1 P Q Rs C)
    thus ?case by(force intro: cSum1)
  next
    case(Sum2 P Q Rs C)
    thus ?case by(force intro: cSum2)
  next
    case(Par1B P a x P' Q C a' x' P'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (P' ∥ Q) = a'<x'> ≺ P''" by fact
    hence aeqa': "a = InputS a'" by(simp add: residualInject)
    have "x' ♯ P ∥ Q" by fact
    hence "x' ♯ P" and "x' ♯ Q" by simp+
    have P''eq: "P'' = ([(x, x')] ∙ P') ∥ Q"
    proof -
      from Eq xineqx' have "(P' ∥ Q) = [(x, x')] ∙ P''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (P' ∥ Q)) = P''" by simp
      with ‹x' ♯ Q›‹x ♯ Q› show ?thesis by(simp add: name_fresh_fresh)
    qed
    
    have "x ♯ P''" by fact
    with P''eq ‹x ≠ x'› have "x' ♯ P'" by(simp add: name_fresh_left name_calc)
    
    have PTrans: "P ⟼a«x» ≺ P'" by fact
    with ‹x' ♯ P'› aeqa' have "P ⟼a'<x'> ≺ ([(x, x')] ∙ P')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C P a' x' ([(x, x')] ∙ P')"
    proof -
      fix C
      have "⋀C a' x' P''. ⟦a«x» ≺ P' = a'<x'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ P'› have "a«x» ≺ P' = a'<x'> ≺ ([(x, x')] ∙ P')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C P a' x' ([(x, x')] ∙ P')" using ‹x' ♯ P› by blast 
    qed
    moreover from PTrans ‹x' ♯ P› have "x' ♯ a" by(auto dest: freshBoundDerivative)
    ultimately have "F C (P ∥ Q) a' x' (([(x, x')] ∙ P') ∥ Q)" using ‹x' ♯ Q›aeqa' ‹x' ♯ P›
      by(rule_tac cPar1B) auto
    with P''eq show ?case by simp
  next
    case(Par1F P P' Q α)
    thus ?case by(simp add: residualInject)
  next
    case(Par2B Q a x Q' P C a' x' Q'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (P ∥ Q') = a'<x'> ≺ Q''" by fact
    hence aeqa': "a = InputS a'" by(simp add: residualInject)
    have "x ♯ P" by fact
    have "x' ♯ P ∥ Q" by fact
    hence "x' ♯ P" and "x' ♯ Q" by simp+
    have Q''eq: "Q'' = P ∥ ([(x, x')] ∙ Q')"
    proof -
      from Eq xineqx' have "(P ∥ Q') = [(x, x')] ∙ Q''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (P ∥ Q')) = Q''" by simp
      with ‹x' ♯ P› ‹x ♯ P› show ?thesis by(simp add: name_fresh_fresh)
    qed
    
    have "x ♯ Q''" by fact
    with Q''eq ‹x ≠ x'› have "x' ♯ Q'" by(simp add: name_fresh_left name_calc)
    
    have QTrans: "Q ⟼a«x» ≺ Q'" by fact
    with ‹x' ♯ Q'› aeqa' have "Q ⟼a'<x'> ≺ ([(x, x')] ∙ Q')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C Q a' x' ([(x, x')] ∙ Q')"
    proof -
      fix C
      have "⋀C a' x' Q''. ⟦a«x» ≺ Q' = a'<x'> ≺ Q''; x' ♯ Q⟧ ⟹ F C Q a' x' Q''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ Q'› have "a«x» ≺ Q' = a'<x'> ≺ ([(x, x')] ∙ Q')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C Q a' x' ([(x, x')] ∙ Q')" using ‹x' ♯ Q›aeqa' by blast 
    qed
    moreover from QTrans ‹x' ♯ Q› have "x' ♯ a" by(force dest: freshBoundDerivative)
    ultimately have "F C (P ∥ Q) a' x' (P ∥ ([(x, x')] ∙ Q'))" using ‹x' ♯ P› aeqa' ‹x' ♯ Q›
      by(rule_tac cPar2B) auto
    with Q''eq show ?case by simp
  next
    case(Par2F P P' Q α)
    thus ?case by(simp add: residualInject)
  next
    case(Comm1 P P' Q Q' a b x)
    thus ?case by(simp add: residualInject)
  next
    case(Comm2 P P' Q Q' a b x)
    thus ?case by(simp add: residualInject)
  next
    case(Close1 P P' Q Q' a x y)
    thus ?case by(simp add: residualInject)
  next
    case(Close2 P P' Q Q' a x y)
    thus ?case by(simp add: residualInject)
  next
    case(ResB P a x P' y C a' x' P'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (<νy>P') = a'<x'> ≺ P''" by fact
    hence aeqa': "a = InputS a'" by(simp add: residualInject)
    have "y ♯ x'" by fact hence yineqx': "y ≠ x'" by simp
    moreover have "x' ♯ <νy>P" by fact
    ultimately have "x' ♯ P" by(simp add: name_fresh_abs)
    have "y ≠ x" and yineqa: "y ♯ a" and yFreshC: "y ♯ C" by fact+
    
    have P''eq: "P'' = <νy>([(x, x')] ∙ P')"
    proof -
      from Eq xineqx' have "<νy>P' = [(x, x')] ∙ P''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (<νy>P')) = P''" by simp
      with yineqx' ‹y ≠ x› show ?thesis by(simp add: name_fresh_fresh)
    qed
    
    have "x ♯ P''" by fact
    with P''eq ‹y ≠ x› ‹x ≠ x'› have "x' ♯ P'" by(simp add: name_fresh_left name_calc name_fresh_abs)
    
    have "P ⟼a«x» ≺ P'" by fact
    with ‹x' ♯ P'› aeqa' have "P ⟼a'<x'> ≺ ([(x, x')] ∙ P')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C P a' x' ([(x, x')] ∙ P')"
    proof -
      fix C
      have "⋀C a' x' P''. ⟦a«x» ≺ P' = a'<x'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ P'› have "a«x» ≺ P' = a'<x'> ≺ ([(x, x')] ∙ P')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C P a' x' ([(x, x')] ∙ P')" using ‹x' ♯ P› aeqa' by blast 
    qed
    ultimately have "F C (<νy>P) a' x' (<νy>([(x, x')] ∙ P'))" using yineqx' yineqa yFreshC aeqa'
      by(force intro: cResB)
    with P''eq show ?case by simp
  next
    case(ResF P P' α y)
    thus ?case by(simp add: residualInject)
  next
    case(Bang P Rs)
    thus ?case by(force intro: cBang)
  qed
qed

lemma boundOutputInduct[consumes 2, case_names Match Mismatch Open Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   F  :: "('a::fs_name) ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes a: "P ⟼a<νx> ≺ P'"
  and       "x ♯ P"
  and     cMatch:    "⋀P a x P' b C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C ([b⌢b]P) a x P'"
  and     cMismatch: "⋀P a x P' b c C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'; b ≠ c⟧ ⟹ F C ([b≠c]P) a x P'"
  and     cOpen:     "⋀P a x P' C.   ⟦P ⟼(OutputR a x) ≺ P'; a ≠ x⟧ ⟹ F C (<νx>P) a x P'"
  and     cSum1:     "⋀P Q a x P' C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C (P ⊕ Q) a x P'" 
  and     cSum2:     "⋀P Q a x Q' C. ⟦Q ⟼a<νx> ≺ Q'; ⋀C. F C Q a x Q'⟧ ⟹ F C (P ⊕ Q) a x Q'" 
  and     cPar1B:    "⋀P P' Q a x C. ⟦P ⟼a<νx> ≺ P'; x ♯ Q; ⋀C. F C P a x P'⟧ ⟹
                                       F C (P ∥ Q) a x (P' ∥ Q)" 
  and     cPar2B:    "⋀P Q Q' a x C. ⟦Q ⟼a<νx> ≺ Q'; x ♯ P; ⋀C. F C Q a x Q'⟧ ⟹
                                       F C (P ∥ Q) a x (P ∥ Q')"
  and     cResB:     "⋀P P' a x y C. ⟦P ⟼a<νx> ≺ P'; y ≠ a; y ≠ x; y ♯ C;
                                       ⋀C. F C P a x P'⟧ ⟹ F C (<νy>P) a x (<νy>P')"
  and     cBang:     "⋀P a x P' C. ⟦P ∥ !P ⟼a<νx> ≺ P'; ⋀C. F C (P ∥ !P) a x P'⟧ ⟹
                                     F C (!P) a x P'"
  shows "F C P a x P'"
proof -
  from a ‹x ♯ P› show ?thesis
  proof(nominal_induct x2 == "a<νx> ≺ P'" avoiding: C a x P' rule: transitions.strong_induct)
    case(Tau P)
    thus ?case by(simp add: residualInject)
  next
    case(Input P a x)
    thus ?case by(simp add: residualInject)
  next
    case(Output P a b)
    thus ?case by(simp add: residualInject)
  next
    case(Match P Rs b C a x)
    thus ?case 
      by(force intro: cMatch simp add: residualInject) 
  next
    case(Mismatch P Rs a b C c x)
    thus ?case 
      by(force intro: cMismatch simp add: residualInject) 
  next
    case(Sum1 P Q Rs C)
    thus ?case by(force intro: cSum1)
  next
    case(Sum2 P Q Rs C)
    thus ?case by(force intro: cSum2)
  next
    case(Open P a b P' C a' x P'')
    have "b ♯ x" by fact hence bineqx: "b ≠ x" by simp
    moreover have "a<νb> ≺ P' = a'<νx> ≺ P''" by fact
    ultimately have aeqa': "a=a'" and P'eqP'': "P'' = [(b, x)] ∙ P'"
      by(simp add: residualInject name_abs_eq)+
    have "x ♯ <νb>P" by fact 
    with bineqx have "x ♯ P" by(simp add: name_fresh_abs)
    have aineqb: "a ≠ b" by fact
    
    have PTrans: "P ⟼a[b] ≺ P'" by fact
    with ‹x ♯ P› have xineqa: "x ≠ a" by(force dest: freshFreeDerivative)
    from PTrans have "([(b, x)] ∙ P) ⟼[(b, x)] ∙ (a[b] ≺ P')" by(rule transitions.eqvt)
    with P'eqP'' xineqa aineqb have Trans: "([(b, x)] ∙ P) ⟼a[x] ≺ P''"
      by(auto simp add: name_calc)
    hence "F C (<νx>([(b, x)] ∙ P)) a x P''" using xineqa by(blast intro: cOpen)
    with ‹x ♯ P› aeqa' show ?case by(simp add: alphaRes)
  next
    case(Par1B P a x P' Q C a' x' P'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (P' ∥ Q) = a'<νx'> ≺ P''" by fact
    hence aeqa': "a = BoundOutputS a'" by(simp add: residualInject)
    have "x ♯ Q" by fact
    have "x' ♯ P ∥ Q" by fact
    hence "x' ♯ P" and "x' ♯ Q" by simp+
    have P''eq: "P'' = ([(x, x')] ∙ P') ∥ Q"
    proof -
      from Eq xineqx' have "(P' ∥ Q) = [(x, x')] ∙ P''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (P' ∥ Q)) = P''" by simp
      with ‹x' ♯ Q›‹x ♯ Q› show ?thesis by(simp add: name_fresh_fresh)
    qed
    
    have "x ♯ P''" by fact
    with P''eq ‹x ≠ x'› have "x' ♯ P'" by(simp add: name_fresh_left name_calc)

    have "P ⟼a«x» ≺ P'" by fact
    with ‹x' ♯ P'› aeqa' have "P ⟼a'<νx'> ≺ ([(x, x')] ∙ P')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C P a' x' ([(x, x')] ∙ P')"
    proof -
      fix C
      have "⋀C a' x' P''. ⟦a«x» ≺ P' = a'<νx'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ P'› have "a«x» ≺ P' = a'<νx'> ≺ ([(x, x')] ∙ P')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C P a' x' ([(x, x')] ∙ P')" using ‹x' ♯ P› aeqa' by blast 
    qed
    ultimately have "F C (P ∥ Q) a' x' (([(x, x')] ∙ P') ∥ Q)" using ‹x' ♯ Q›aeqa'
      by(blast intro: cPar1B)
    with P''eq show ?case by simp
  next
    case(Par1F P P' Q α)
    thus ?case by(simp add: residualInject)
  next
    case(Par2B Q a x Q' P C a' x' Q'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (P ∥ Q') = a'<νx'> ≺ Q''" by fact
    hence aeqa': "a = BoundOutputS a'" by(simp add: residualInject)
    have "x ♯ P" by fact
    have "x' ♯ P ∥ Q" by fact
    hence "x' ♯ P" and "x' ♯ Q" by simp+
    have Q''eq: "Q'' = P ∥ ([(x, x')] ∙ Q')"
    proof -
      from Eq xineqx' have "(P ∥ Q') = [(x, x')] ∙ Q''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (P ∥ Q')) = Q''" by simp
      with ‹x' ♯ P› ‹x ♯ P› show ?thesis by(simp add: name_fresh_fresh)
    qed
    
    have "x ♯ Q''" by fact
    with Q''eq ‹x ≠ x'› have "x' ♯ Q'" by(simp add: name_fresh_left name_calc)

    have "Q ⟼a«x» ≺ Q'" by fact
    with ‹x' ♯ Q'› aeqa' have "Q ⟼a'<νx'> ≺ ([(x, x')] ∙ Q')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C Q a' x' ([(x, x')] ∙ Q')"
    proof -
      fix C
      have "⋀C a' x' Q''. ⟦a«x» ≺ Q' = a'<νx'> ≺ Q''; x' ♯ Q⟧ ⟹ F C Q a' x' Q''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ Q'› have "a«x» ≺ Q' = a'<νx'> ≺ ([(x, x')] ∙ Q')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C Q a' x' ([(x, x')] ∙ Q')" using ‹x' ♯ Q›aeqa' by blast 
    qed
    ultimately have "F C (P ∥ Q) a' x' (P ∥ ([(x, x')] ∙ Q'))" using ‹x' ♯ P›
      by(blast intro: cPar2B)
    with Q''eq show ?case by simp
  next
    case(Par2F P P' Q α)
    thus ?case by(simp add: residualInject)
  next
    case(Comm1 P P' Q Q' a b x)
    thus ?case by(simp add: residualInject)
  next
    case(Comm2 P P' Q Q' a b x)
    thus ?case by(simp add: residualInject)
  next
    case(Close1 P P' Q Q' a x y)
    thus ?case by(simp add: residualInject)
  next
    case(Close2 P P' Q Q' a x y)
    thus ?case by(simp add: residualInject)
  next
    case(ResB P a x P' y C a' x' P'')
    have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
    moreover have Eq: "a«x» ≺ (<νy>P') = a'<νx'> ≺ P''" by fact
    hence aeqa': "a = BoundOutputS a'" by(simp add: residualInject)
    have "y ♯ x'" by fact hence yineqx': "y ≠ x'" by simp
    moreover have "x' ♯ <νy>P" by fact
    ultimately have "x' ♯ P" by(simp add: name_fresh_abs)
    have "y ≠ x" and "y ♯ a" and yFreshC: "y ♯ C" by fact+

    have P''eq: "P'' = <νy>([(x, x')] ∙ P')"
    proof -
      from Eq xineqx' have "<νy>P' = [(x, x')] ∙ P''"
        by(simp add: residualInject name_abs_eq)
      hence "([(x, x')] ∙ (<νy>P')) = P''" by simp
      with yineqx' ‹y ≠ x› show ?thesis by(simp add: name_fresh_fresh)
    qed

    have "x ♯ P''" by fact
    with P''eq ‹y ≠ x› ‹x ≠ x'› have "x' ♯ P'" by(simp add: name_fresh_left name_calc name_fresh_abs)

    have "P ⟼a«x» ≺ P'" by fact
    with ‹x' ♯ P'› aeqa' have "P ⟼a'<νx'> ≺ ([(x, x')] ∙ P')"
      by(simp add: alphaBoundResidual)
    moreover have "⋀C. F C P a' x' ([(x, x')] ∙ P')"
    proof -
      fix C
      have "⋀C a' x' P''. ⟦a«x» ≺ P' = a'<νx'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
      moreover with aeqa' xineqx' ‹x' ♯ P'› have "a«x» ≺ P' = a'<νx'> ≺ ([(x, x')] ∙ P')"
        by(simp add: residualInject name_abs_eq name_fresh_left name_calc)
      ultimately show "F C P a' x' ([(x, x')] ∙ P')" using ‹x' ♯ P› aeqa' by blast 
    qed
    ultimately have "F C (<νy>P) a' x' (<νy>([(x, x')] ∙ P'))" using yineqx' ‹y ♯ a› yFreshC aeqa'
      by(force intro: cResB)
    with P''eq show ?case by simp
  next
    case(ResF P P' α y)
    thus ?case by(simp add: residualInject)
  next
    case(Bang P Rs)
    thus ?case by(force intro: cBang)
  qed
qed

lemma tauInduct[consumes 1, case_names Tau Match Mismatch Sum1 Sum2 Par1 Par2 Comm1 Comm2 Close1 Close2 Res Bang]:
  fixes P  :: pi
  and   P' :: pi
  and   F  :: "'a::fs_name ⇒ pi ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P ⟼τ ≺ P'"
  and     "⋀P C. F C (τ.(P)) P"
  and     "⋀P P' c C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C ([c⌢c]P) P'"
  and     "⋀P P' c d C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'; c ≠ d⟧ ⟹ F C ([c≠d]P) P'"
  and     "⋀P P' Q C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C (P ⊕ Q) P'"
  and     "⋀Q Q' P C. ⟦Q ⟼τ ≺ Q'; ⋀C. F C Q Q'⟧ ⟹ F C (P ⊕ Q) Q'"
  and     "⋀P P' Q C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C (P ∥ Q) (P' ∥ Q)"
  and     "⋀Q Q' P C. ⟦Q ⟼τ ≺ Q'; ⋀C. F C Q Q'⟧ ⟹ F C (P ∥ Q) (P ∥ Q')"
  and     "⋀P a x P' Q b Q' C. ⟦P ⟼(BoundR (InputS a) x P'); Q ⟼OutputR a b ≺ Q'; x ♯ P; x ♯ Q; x ♯ C⟧ ⟹ F C (P ∥ Q) (P'[x::=b] ∥ Q')"
  and     "⋀P a b P' Q x Q' C. ⟦P ⟼OutputR a b ≺ P'; Q ⟼(BoundR (InputS a) x Q'); x ♯ P; x ♯ Q; x ♯ C⟧ ⟹ F C (P ∥ Q) (P' ∥ Q'[x::=b])"
  and     "⋀P a x P' Q y Q' C. ⟦P ⟼(BoundR (InputS a) x P'); Q ⟼a<νy> ≺ Q'; x ♯ P; x ♯ Q; x ♯ C; y ♯ P; y ♯ Q; y ♯ C; x ≠ y⟧ ⟹ F C (P ∥ Q) (<νy>(P'[x::=y] ∥ Q'))"
  and     "⋀P a y P' Q x Q' C. ⟦P ⟼a<νy> ≺ P'; Q ⟼(BoundR (InputS a) x Q'); x ♯ P; x ♯ Q; x ♯ C; y ♯ P; y ♯ Q; y ♯ C; x ≠ y⟧ ⟹ F C (P ∥ Q) (<νy>(P' ∥ Q'[x::=y]))"
  and     "⋀P P' x C. ⟦P ⟼τ ≺ P'; x ♯ C; ⋀C. F C P P'⟧ ⟹
                        F C (<νx>P) (<νx>P')"
  and     "⋀P P' C. ⟦P ∥ !P ⟼τ ≺ P'; ⋀C. F C (P ∥ !P) P'⟧ ⟹ F C (!P) P'"

  shows "F C P P'"
proof -
  from Trans show ?thesis
    by(nominal_induct x2=="τ ≺ P'" avoiding: C arbitrary: P' rule: transitions.strong_induct,
       auto simp add: residualInject intro: assms)
qed

inductive bangPred :: "pi ⇒ pi ⇒ bool"
where
  aux1: "bangPred P (!P)"
| aux2: "bangPred P (P ∥ !P)"

inductive_cases nilCases'[simplified pi.distinct residual.distinct]: "𝟬 ⟼ Rs"
inductive_cases tauCases'[simplified pi.distinct residual.distinct]: "τ.(P) ⟼ Rs"
inductive_cases inputCases'[simplified pi.inject residualInject]: "a<b>.P ⟼ Rs"
inductive_cases outputCases'[simplified pi.inject residualInject]: "a{b}.P ⟼ Rs"
inductive_cases matchCases'[simplified pi.inject residualInject]: "[a⌢b]P ⟼ Rs"
inductive_cases mismatchCases'[simplified pi.inject residualInject]: "[a≠b]P ⟼ Rs"
inductive_cases sumCases'[simplified pi.inject residualInject]: "P ⊕ Q ⟼ Rs"
inductive_cases parCasesB'[simplified pi.distinct residual.distinct]: "P ∥ Q ⟼ b«y» ≺ P'"
inductive_cases parCasesF'[simplified pi.distinct residual.distinct]: "P ∥ Q ⟼ α ≺ P'"
inductive_cases resCases'[simplified pi.distinct residual.distinct]: "<νx>P ⟼ Rs"
inductive_cases resCasesB'[simplified pi.distinct residual.distinct]: "<νx'>P ⟼ a«y'» ≺ P'"
inductive_cases resCasesF'[simplified pi.distinct residual.distinct]: "<νx>P ⟼ α ≺ P'"
inductive_cases bangCases[simplified pi.distinct residual.distinct]: "!P ⟼ Rs"

lemma tauCases[consumes 1, case_names cTau]:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "τ.(P) ⟼α ≺ P'"
  and "⟦α = τ; P = P'⟧ ⟹ Prop (τ) P"

  shows "Prop α P'"
using assms
by(erule_tac tauCases', auto simp add: pi.inject residualInject)

lemma outputCases[consumes 1, case_names cOutput]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "a{b}.P ⟼α ≺ P'"
  and "⟦α = a[b]; P = P'⟧ ⟹ Prop (a[b]) P"

  shows "Prop α P'"
using assms
by(erule_tac outputCases', auto simp add: residualInject)

lemma zeroTrans[dest]:
  fixes Rs :: residual

  assumes "𝟬 ⟼ Rs"

  shows "False"
using assms
by(induct rule: nilCases', auto)

lemma resZeroTrans[dest]:
  fixes x  :: name
  and   Rs :: residual

  assumes "<νx>𝟬 ⟼ Rs"

  shows "False"
using assms
by(induct rule: resCases', auto simp add: pi.inject alpha')

lemma matchTrans[dest]:
  fixes a   :: name
  and   b   :: name
  and   P   :: pi
  and   Rs  :: residual

  assumes "[a⌢b]P ⟼ Rs"
  and     "a≠b"

  shows "False"
using assms
by(induct rule: matchCases', auto)

lemma mismatchTrans[dest]:
  fixes a   :: name
  and   P   :: pi
  and   Rs  :: residual

  assumes "[a≠a]P ⟼ Rs"

  shows "False"
using assms
by(induct rule: mismatchCases', auto)

lemma inputCases[consumes 4, case_names cInput]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   P' :: pi

  assumes Input: "a<x>.P ⟼ b«y» ≺ yP'"
  and     "y ≠ a"
  and     "y ≠ x"
  and     "y ♯ P"
  and     A:     "⟦b = InputS a; yP' = ([(x, y)] ∙ P)⟧  ⟹ Prop (InputS a) y ([(x, y)] ∙ P)"

  shows "Prop b y yP'"
proof -
  note assms
  moreover from Input ‹y ≠ a› ‹y ≠ x› ‹y ♯ P› have "y ♯ b"
    by(force dest: freshBoundDerivative simp add: abs_fresh)
  moreover obtain z::name where "z ≠ y" and "z ≠ x" and "z ♯ P" and "z ≠ a" and "z ♯ b" and "z ♯ yP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  moreover obtain z'::name where "z' ≠ y" and "z' ≠ x" and "z' ≠ z" and "z' ♯ P" and "z' ≠ a" and "z' ♯ b" and "z' ♯ yP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  ultimately show ?thesis
    by(cases rule: transitions.strong_cases[where x=y and b=z and xa=z and xb=z and xc=z and xd=z and xe=z
                                            and xf=z and xg=z and y=z' and ya=z' and yb=y and yc=z'])
      (auto simp add: pi.inject residualInject alpha abs_fresh fresh_prod fresh_left calc_atm)+
qed

lemma tauBoundTrans[dest]:
  fixes P  :: pi
  and   a  :: subject
  and   x  :: name
  and   P' :: pi

  assumes "τ.(P) ⟼a«x» ≺ P'"

  shows False
using assms
by - (ind_cases "τ.(P) ⟼a«x» ≺ P'") 

lemma tauOutputTrans[dest]:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes "τ.(P) ⟼a[b] ≺ P'"

  shows False
using assms
by - (ind_cases "τ.(P) ⟼a[b] ≺ P'", auto simp add: residualInject) 

lemma inputFreeTrans[dest]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  
  assumes "a<x>.P ⟼α ≺ P'"

  shows False
using assms
by - (ind_cases "a<x>.P ⟼α ≺ P'")

lemma inputBoundOutputTrans[dest]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   b  :: name
  and   y  :: name
  and   P' :: pi

  assumes "a<x>.P ⟼b<νy> ≺ P'"

  shows False
using assms
by - (ind_cases "a<x>.P ⟼b<νy> ≺ P'", auto simp add: residualInject)

lemma outputTauTrans[dest]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   P' :: pi

  assumes "a{b}.P ⟼τ ≺ P'"

  shows False
using assms
by - (ind_cases "a{b}.P ⟼τ ≺ P'", auto simp add: residualInject)

lemma outputBoundTrans[dest]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   c  :: subject
  and   x  :: name
  and   P' :: pi

  assumes "a{b}.P ⟼c«x» ≺ P'"

  shows False
using assms
by - (ind_cases "a{b}.P ⟼c«x» ≺ P'")

lemma outputIneqTrans[dest]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   c  :: name
  and   d  :: name
  and   P' :: pi

  assumes "a{b}.P ⟼c[d] ≺ P'"
  and     "a ≠ c ∨ b ≠ d"

  shows "False"
using assms
by - (ind_cases "a{b}.P ⟼c[d] ≺ P'", auto simp add: residualInject pi.inject alpha')

lemma outputFreshTrans[dest]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "a{b}.P ⟼α ≺ P'"
  and     "a ♯ α ∨ b ♯ α"

  shows "False"
using assms
by - (ind_cases "a{b}.P ⟼α ≺ P'", auto simp add: residualInject pi.inject alpha')

lemma inputIneqTrans[dest]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   b  :: subject
  and   y  :: name
  and   P' :: pi

  assumes "a<x>.P ⟼b«y» ≺ P'"
  and     "a ♯ b"

  shows "False"
using assms
by - (ind_cases "a<x>.P ⟼b«y» ≺ P'", auto simp add: residualInject pi.inject)

lemma resTauBoundTrans[dest]:
  fixes x  :: name
  and   P  :: pi
  and   a  :: subject
  and   y  :: name
  and   P' :: pi

  assumes "<νx>τ.(P) ⟼a«y» ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>τ.(P) ⟼a«y» ≺ P'", auto simp add: residualInject pi.inject alpha')

lemma resTauOutputTrans[dest]:
  fixes x  :: name
  and   P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes "<νx>τ.(P) ⟼a[b] ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>τ.(P) ⟼a[b] ≺ P'", auto simp add: residualInject pi.inject alpha')

lemma resInputFreeTrans[dest]:
  fixes x  :: name
  fixes a  :: name
  and   y  :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  
  assumes "<νx>a<y>.P ⟼α ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>a<y>.P ⟼α ≺ P'", auto simp add: pi.inject residualInject alpha')

lemma resInputBoundOutputTrans[dest]:
  fixes x  :: name
  and   a  :: name
  and   y  :: name
  and   P  :: pi
  and   b  :: name
  and   z  :: name
  and   P' :: pi

  assumes "<νx>a<y>.P ⟼b<νz> ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>a<y>.P ⟼b<νz> ≺ P'", auto simp add: pi.inject residualInject alpha')

lemma resOutputTauTrans[dest]:
  fixes x  :: name
  and   a  :: name
  and   b  :: name
  and   P  :: pi
  and   P' :: pi

  assumes "<νx>a{b}.P ⟼τ ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>a{b}.P ⟼τ ≺ P'", auto simp add: residualInject pi.inject alpha')

lemma resOutputInputTrans[dest]:
  fixes x  :: name
  and   a  :: name
  and   b  :: name
  and   P  :: pi
  and   c  :: name
  and   y  :: name
  and   P' :: pi

  assumes "<νx>a{b}.P ⟼c<y> ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>a{b}.P ⟼c<y> ≺ P'", auto simp add: pi.inject residualInject alpha')

lemma resOutputOutputTrans[dest]:
  fixes x  :: name
  and   a  :: name
  and   P  :: pi
  and   b  :: name
  and   y  :: name
  and   P' :: pi
  
  assumes "<νx>a{x}.P ⟼b[y] ≺ P'"

  shows False
using assms
by - (ind_cases "<νx>a{x}.P ⟼b[y] ≺ P'", auto simp add: pi.inject residualInject alpha' calc_atm)

lemma resTrans[dest]:
  fixes x  :: name
  and   b  :: name
  and   Rs :: residual
  and   y  :: name

  shows "<νx>x{b}.P ⟼ Rs ⟹ False"
  and   "<νx>x<y>.P ⟼ Rs ⟹ False"
apply(ind_cases "<νx>x{b}.P ⟼ Rs", auto simp add: pi.inject alpha' calc_atm)
by(ind_cases "<νx>x<y>.P ⟼ Rs", auto simp add: pi.inject alpha' calc_atm abs_fresh fresh_left)

lemma matchCases[consumes 1, case_names cMatch]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name ⇒ name ⇒ bool"

  assumes "[a⌢b]P ⟼ Rs"
  and     "⟦P ⟼ Rs; a = b⟧ ⟹ F a a"

  shows "F a b"
using assms
by(induct rule: matchCases', auto)

lemma mismatchCases[consumes 1, case_names cMismatch]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name ⇒ name ⇒ bool"

  assumes Trans:  "[a≠b]P ⟼ Rs"
  and     cMatch: "⟦P ⟼ Rs; a ≠ b⟧ ⟹ F a b"

  shows "F a b"
using assms
by(induct rule: mismatchCases', auto)

lemma sumCases[consumes 1, case_names cSum1 cSum2]:
  fixes P  :: pi
  and   Q  :: pi
  and   Rs :: residual

  assumes Trans: "P ⊕ Q ⟼ Rs"
  and     cSum1: "P ⟼ Rs ⟹ Prop"
  and     cSum2: "Q ⟼ Rs ⟹ Prop"

  shows Prop
using assms
by(induct rule: sumCases', auto)

lemma name_abs_alpha:
  fixes a :: name
  and   b :: name
  and   P :: pi
  
  assumes "b ♯ P"

  shows "[a].P = [b].([(a, b)] ∙ P)"
proof(cases "a=b", auto)
  assume "a ≠ b"
  with assms show ?thesis
    by(force intro: abs_fun_eq3[OF pt_name_inst, OF at_name_inst]
             simp add: name_swap name_calc name_fresh_left)
qed

lemma parCasesB[consumes 3, case_names cPar1 cPar2]:
  fixes P   :: pi
  and   Q   :: pi
  and   a   :: subject
  and   x   :: name
  and   PQ' :: pi
  and   C   :: "'a::fs_name"
  
  assumes "P ∥ Q ⟼ a«x» ≺ PQ'"
  and     "x ♯ P"
  and     "x ♯ Q"
  and     "⋀P'. P ⟼ a«x» ≺ P' ⟹ Prop (P' ∥ Q)"
  and     "⋀Q'. Q ⟼ a«x» ≺ Q' ⟹ Prop (P ∥ Q')"

  shows "Prop PQ'"
proof -
  note assms
  moreover from ‹P ∥ Q ⟼a«x» ≺ PQ'› ‹x ♯ P› ‹x ♯ Q› have "x ♯ a"
    by(force dest: freshBoundDerivative)
  moreover obtain y::name where "y ≠ x" and "y ♯ P" and "y ♯ Q" and "y ♯ a" and "y ♯ PQ'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  moreover obtain z::name where "z ≠ y" and "z ≠ x" and "z ♯ P" and "z ♯ Q" and "z ♯ a" and "z ♯ PQ'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  ultimately show ?thesis
    by(cases rule: transitions.strong_cases[where x=y and b=y and xa=x and xb=x and xc=y and xd=y and xe=y
                                              and xf=y and xg=y and y=z and ya = z and yb=z and yc=z])
      (auto simp add: pi.inject residualInject alpha abs_fresh fresh_prod)+
qed


lemma parCasesF[consumes 1, case_names cPar1 cPar2 cComm1 cComm2 cClose1 cClose2]:
  fixes P  :: pi
  and   Q  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   C  :: "'a::fs_name"
  and   F  :: "freeRes ⇒ pi ⇒ bool"

  assumes Trans: "P ∥ Q ⟼ α ≺ PQ'"
  and     icPar1F: "⋀P'. ⟦P ⟼ α ≺ P'⟧ ⟹ F α (P' ∥ Q)"
  and     icPar2F: "⋀Q'. ⟦Q ⟼ α ≺ Q'⟧ ⟹ F α (P ∥ Q')"
  and     icComm1: "⋀P' Q' a b x. ⟦P ⟼ a<x> ≺ P'; Q ⟼ a[b] ≺ Q'; x ♯ P; x♯ Q; x ≠ a; x ≠ b; x ♯ Q'; x ♯ C; α = τ⟧ ⟹ F (τ) (P'[x::=b] ∥ Q')"
  and     icComm2: "⋀P' Q' a b x. ⟦P ⟼ a[b] ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ≠ b; x ♯ P'; x ♯ C; α = τ⟧ ⟹ F (τ) (P' ∥ Q'[x::=b])"
  and     icClose1: "⋀P' Q' a x y. ⟦P ⟼ a<x> ≺ P'; Q ⟼ a<νy> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ≠ y; x ♯ Q'; y ♯ P; y ♯ Q; y ≠ a; y ♯ P'; x ♯ C; y ♯ C; α = τ⟧ ⟹ 
                                     F (τ) (<νy>(P'[x::=y] ∥ Q'))"
  and     icClose2: "⋀P' Q' a x y. ⟦P ⟼ a<νy> ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ≠ y; x ♯ P'; y ♯ P; y ♯ Q; y ≠ a; y ♯ Q'; x ♯ C; y ♯ C; α = τ⟧ ⟹
                                      F (τ) (<νy>(P' ∥ Q'[x::=y]))"

  shows "F α PQ'"
proof -
  note assms
  moreover obtain x::name where "x ♯ P" and "x ♯ Q" and "x ♯ α" and "x ♯ PQ'" and "x ♯ C"
    by(generate_fresh "name", auto simp add: fresh_prod)
  moreover obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ α" and "y ♯ PQ'" and "y ♯ C" and "x ≠ y"
    by(generate_fresh "name", auto simp add: fresh_prod)
  ultimately show ?thesis
    by(cases rule: transitions.strong_cases[where x=x and b=x and xa=x and xb=x and xc=x and xd=x and xe=x
                                              and xf=x and xg=x and y=y and ya=y and yb=y and yc=y])
      (auto simp add: pi.inject residualInject alpha abs_fresh fresh_prod)+
qed

lemma resCasesF[consumes 1, case_names cRes]:
  fixes x  :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   C  :: "'a::fs_name"

  assumes "<νx>P ⟼ α ≺ xP'"
  and     "⋀P'. ⟦P ⟼ α ≺ P'; x ♯ α⟧ ⟹ F (<νx>P')"

  shows "F xP'"
proof -
  note assms
  moreover from ‹<νx>P ⟼α ≺ xP'› have "x ♯ α" and "x ♯ xP'"
    by(force dest: freshFreeDerivative simp add: abs_fresh)+
  moreover obtain y::name where "y ≠ x" and "y ♯ P" and "y ♯ α" and "y ♯ xP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  moreover obtain z::name where "z ≠ y" and "z ≠ x" and "z ♯ P" and "z ♯ α" and "z ♯ xP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  ultimately show ?thesis
    by(cases rule: transitions.strong_cases[where x=y and b=y and xa=y and xb=y and xc=y and xd=y and xe=y
                                              and xf=y and xg=y and y=z and ya=z and yb=z and yc=x])
      (auto simp add: pi.inject residualInject alpha abs_fresh fresh_prod)+
qed

lemma resCasesB[consumes 3, case_names cOpen cRes]:
  fixes x :: name
  and   P  :: pi
  and   a  :: subject
  and   y :: name
  and   yP' :: pi
  and   C  :: "'a::fs_name"

  assumes Trans:  "<νy>P ⟼a«x» ≺ yP'"
  and     xineqy: "x ≠ y"
  and     xineqy: "x ♯ P"
  and     rcOpen: "⋀b P'. ⟦P ⟼b[y] ≺ P'; b ≠ y; a = BoundOutputS b⟧ ⟹ F (BoundOutputS b) ([(x, y)] ∙ P')"
  and     rcResB: "⋀P'. ⟦P ⟼ a«x» ≺ P'; y ♯ a⟧ ⟹ F a (<νy>P')"

  shows "F a yP'"
proof -
  note assms
  moreover from ‹<νy>P ⟼a«x» ≺ yP'› ‹x ≠ y› have "y ♯ a" and "y ♯ yP'"
    by(force dest: freshBoundDerivative simp add: abs_fresh)+
  moreover from  ‹<νy>P ⟼a«x» ≺ yP'› ‹x ♯ P› have "x ♯ a"
    by(force dest: freshBoundDerivative simp add: abs_fresh)+
  moreover obtain z::name where "z ≠ y" and "z ≠ x" and "z ♯ P" and "z ♯ a" and "z ♯ yP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  moreover obtain z'::name where "z' ≠ y" and "z' ≠ x" and "z' ≠ z" and "z' ♯ P" and "z' ♯ a" and "z' ♯ yP'" 
    by(generate_fresh "name", auto simp add: fresh_prod)
  ultimately show ?thesis
    by(cases rule: transitions.strong_cases[where x=z and b=y and xa=z and xb=z and xc=z and xd=z and xe=z
                                              and xf=z and xg=x and y=z' and ya=z' and yb=y and yc=z'])
      (auto simp add: pi.inject residualInject alpha abs_fresh fresh_prod fresh_left calc_atm)+
qed

lemma bangInduct[consumes 1, case_names cPar1B cPar1F cPar2B cPar2F cComm1 cComm2 cClose1 cClose2 cBang]:
  fixes F  :: "'a::fs_name ⇒ pi ⇒ residual ⇒ bool"
  and   P  :: pi
  and   Rs :: residual
  and   C  :: "'a::fs_name"

  assumes Trans:  "!P ⟼ Rs"
  and     cPar1B: "⋀a x P' C. ⟦P ⟼ a«x» ≺ P'; x ♯ P; x ♯ C⟧ ⟹ F C (P ∥ !P) (a«x» ≺ P' ∥ !P)"
  and     cPar1F: "⋀α P' C. ⟦P ⟼ α ≺ P'⟧ ⟹ F C (P ∥ !P) (α ≺ P' ∥ !P)"
  and     cPar2B: "⋀a x P' C. ⟦!P ⟼ a«x» ≺ P'; x ♯ P; x ♯ C; ⋀C. F C (!P) (a«x» ≺ P')⟧ ⟹ 
                               F C (P ∥ !P) (a«x» ≺ P ∥ P')"
  and     cPar2F: "⋀α P' C. ⟦!P ⟼ α ≺ P'; ⋀C. F C (!P) (α ≺ P')⟧ ⟹ F C (P ∥ !P) (α ≺ P ∥ P')"
  and     cComm1: "⋀a x P' b P'' C. ⟦P ⟼ a<x> ≺ P'; !P ⟼ (OutputR a b) ≺ P''; x ♯ C;
                                      ⋀C. F C (!P) ((OutputR a b) ≺ P'')⟧ ⟹
                                      F C (P ∥ !P) (τ ≺ (P'[x::=b]) ∥ P'')"
  and     cComm2: "⋀a b P' x P'' C. ⟦P ⟼ (OutputR a b) ≺ P'; !P ⟼ a<x> ≺ P''; x ♯ C; 
                                      ⋀C. F C (!P) (a<x> ≺ P'')⟧ ⟹
                                      F C (P ∥ !P) (τ ≺ P' ∥ (P''[x::=b]))"
  and     cClose1: "⋀a x P' y P'' C. ⟦P ⟼ a<x> ≺ P'; !P ⟼ a<νy> ≺ P''; y ♯ P; x ♯ C; y ♯ C;
                                      ⋀C. F C (!P) (a<νy> ≺ P'')⟧ ⟹
                                      F C (P ∥ !P) (τ ≺ <νy>((P'[x::=y]) ∥ P''))"
  and     cClose2: "⋀a y P' x P'' C. ⟦P ⟼ a<νy> ≺ P'; !P ⟼ a<x> ≺ P''; y ♯ P; x ♯ C; y ♯ C;
                                       ⋀C. F C (!P) (a<x> ≺ P'')⟧ ⟹
                                       F C (P ∥ !P) (τ ≺ <νy>(P' ∥ (P''[x::=y])))"
  and     cBang: "⋀Rs C. ⟦P ∥ !P ⟼ Rs; ⋀C. F C (P ∥ !P) Rs⟧ ⟹ F C (!P) Rs"

  shows "F C (!P) Rs"
proof -
  have "⋀X Y C. ⟦X ⟼ Y; bangPred P X⟧ ⟹ F C X Y"
  proof -
    fix X Y C
    assume "X ⟼ Y" and "bangPred P X"
    thus "F C X Y"
    proof(nominal_induct avoiding: C rule: transitions.strong_induct)
      case(Tau Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (τ.(Pa))")
    next
      case(Input x a Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (a<x>.Pa)")
    next
      case(Output a b Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (a{b}.Pa)")
    next
      case(Match Pa Rs b)
      thus ?case
        apply -
        by(ind_cases "bangPred P ([b⌢b]Pa)")
    next
      case(Mismatch Pa Rs a b)
      thus ?case
        apply -
        by(ind_cases "bangPred P ([a≠b]Pa)")
    next
      case(Open Pa a b Pa')
      thus ?case
        apply -
        by(ind_cases "bangPred P (<νb>Pa)")
    next
      case(Sum1 Pa Rs Q)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ⊕ Q)")
    next
      case(Sum2 Q Rs Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ⊕ Q)")
    next
      case(Par1B Pa a x Pa' Q )
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cPar1B simp add: pi.inject)
    next
      case(Par1F Pa α Pa' Q)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cPar1F simp add: pi.inject)
    next
      case(Par2B Qa a x Qa' Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Qa)", auto intro: cPar2B aux1 simp add: pi.inject)
    next
      case(Par2F Qa α Qa' Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Qa)", auto intro: cPar2F aux1 simp add: pi.inject)
    next
      case(Comm1 Pa a x Pa' Q b Q')
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cComm1 aux1 simp add: pi.inject)
    next
      case(Comm2 Pa a b Pa' Q x Q')
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cComm2 aux1 simp add: pi.inject)
    next
      case(Close1 Pa a x Pa' Q y Q')
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cClose1 aux1 simp add: pi.inject)
    next
      case(Close2 Pa a y Pa' Q x Q')
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: cClose2 aux1 simp add: pi.inject)
    next
      case(ResB Pa a x P' y)
      thus ?case
        apply -
        by(ind_cases "bangPred P (<νy>Pa)")
    next
      case(ResF Pa α P' y)
      thus ?case
        apply -
        by(ind_cases "bangPred P (<νy>Pa)")
    next
      case(Bang Pa Rs)
      thus ?case
        apply -
        by(ind_cases "bangPred P (!Pa)", auto intro: cBang aux2 simp add: pi.inject)
    qed
  qed

  with Trans show ?thesis by(force intro: bangPred.aux1)
qed

end